\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $L$:(Id List), $e$:es{-}E(${\it es}$).
\\[0ex]fischer\=\{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2\}\+
\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\Rightarrow$ f{-}newround\=\{x:ut2, free:ut2, mine:ut2\}\+
\\[0ex](${\it es}$; $L$; $e$)
\-\\[0ex]$\Rightarrow$ f{-}event\=\{x:ut2\}\+
\\[0ex](${\it es}$; $L$; $e$)
\-
\end{tabbing}